T, T':Type, a:(T List), f, g:(TT').
(i:. (i < ||a||)  (f(a[i]) = g(a[i])))  (map(f;a) = map(g;a)  (T' List)) 

latex

Definitions	False, A, A  B, , t  T, P  Q, x:A. B(x), P  Q, P  Q, P & Q, i  j < k, {i..j},
Lemmas	select wf, length wf1, nat wf, map wf, list extensionality, map length, map select, le wf